es:ES, e, e':E. (e <loc e')  ([e, e'] ~ ([e, pred(e')] @ [e'])) 

latex

Definitions	x:A. B(x), P  Q, [e, e'], filter(P;l), before(e), t  T, Y, if b t else f fi, true, false, Prop, reduce(f;k;as), e  e' , P  Q, , A, P & Q, P  Q, Unit, False, P  Q,
Lemmas	filter append, es-ble wf, es-before wf, es-pred wf, es-locl-iff, es-first wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, es-locl wf, es-E wf, event system wf, assert-es-ble